COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%business letter outline to use with buslet.tex macros
C00008 ENDMK
C⊗;
%business letter outline to use with buslet.tex macros
\magnification =\magstephalf
\input buslet[1,ra]
\def\disleft#1:#2:#3\par{\par\hangindent#1\noindent
			 \hbox to #1{#2 \hfill \hskip .1em}\ignorespaces#3\par}
\def\display#1:#2:#3\par{\par\hangindent #1 \noindent
			\hbox to #1{\hfill #2 \hskip .1em}\ignorespaces#3 \par}
\def\adx#1:#2\par{\par\halign{\hskip #1##\hfill\cr #2}\par}


\jmclet

\vskip 30pt
\address 
Mr. W.T. Chien    
Program Director  
Intelligent Systems
Division of Computer Science
National Science Foundation
1800 G Street N.W.
Washington, D.C. 20550
\body
Re: NSF PROGRESS REPORT, MCS 82-06565

Dear Mr. Chien:    

Dr. Jussi Ketonen has been working on further development of EKL,
an interactive proof checker in high order predicate calculus.
He has been on a leave of absence for the academic year 84-85,
working on compiler optimization techniques for Common Lisp
Compilers. Some of this work has been based on his study of type
structures.
	
ACCOMPLISHMENTS FOR THE ACADEMIC YEAR 84-85:

	The paper of Ketonen and Weyhrauch, titled
``A Decidable Fragment of Predicate Calculus'', was published in 
the Journal of Theoretical Computer Science, vol 32, pp.297-307 (1984).

	The paper of Ketonen, titled
``EKL---A Mathematically Oriented Proof Checker'',
was published in the Proceedings of the Seventh International
Conference on Automatic Deduction, Lecture Notes in Computer Science, Vol. 170,
pp.65-79, Springer Verlag (1984).

        Ketonen and Weening have published a manual for EKL, titled
``EKL - An Interactive Proof Checker, User's Reference Guide'', 
as Computer Science Department Report No. STAN-CS-83-992 (June 1984).

	EKL has been used in courses on Lisp programming
during the academic year of 1983-84 at Stanford.
As homework assignments, students used it to prove facts about Lisp programs.

	Gian-Luigi Bellin, a graduate student in the Philosophy Department,
has been working on implementing Landau's ``Grundlagen der Mathematik'' and
proving facts about finite functions. The latter mentioned work has progressed
jointly with Ketonen during his leave of absence. Ketonen and Bellin are
planning on publishing the results of this research this fall.

\eject
PLANS FOR THE NEXT ACADEMIC YEAR

Ketonen plans to:

	(1) apply the techniques for proof checking that he has
developed to verifying a large class of mathematical facts and 
Lisp programs. 

	(2) to continue his research on logical algorithms, in
particular the decision procedure described by Ketonen and Weyhrauch.
Many interesting problems remain: For example, the proper use 
of equalities in the decision procedure mentioned above and
its correct implementation. 
 
	(3) to study further refinements of the language of EKL.
This will be joint work with Bellin. The plan is to extend the
definitional capacities of EKL towards more powerful high order
axioms. The ultimate outcome of this research will be a even
more general and flexible language for EKL.


\closing
Sincerely,    

John McCarthy    
\annotations
\vskip 1in
JMC/ra 
%\smallskip
%Enclosure
%\smallskip
%cc: Matthew Kahn
%\smallskip
%\ps
%P.S.: whatever you wish to say here

\endletter

\makelabel
\end